COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	\magnification\magstephalf
C00009 ENDMK
C⊗;
\magnification\magstephalf
\input macro.tex
\def\today{\ifcase\month\or
  January\or February\or March\or April\or May\or June\or
  July\or August\or September\or October\or November\or December\fi
  \space\number\day, \number\year}
\baselineskip 14pt
\rm
\line{\sevenrm a60 tex[154,phy] \today\hfill}

\parskip 5pt
\line{\bf The First-order Calculus is Undecidable --- Short Proof\hfil}

\medskip
An {\it oblivious two-counter machine\/} (OTCM) is a computer with a finite
number of control states, and two registers $K↓1$ and~$K↓2$ containing
natural numbers, with a repertory of instructions limited to:

\smallskip
\disleft 20pt:$\bullet$:
{\tt START}, set $K↓1=K↓2=0$, go to $A$.

\disleft 20pt:$\bullet$:
$K↓1←K↓1+1$, go to $A$.

\disleft 20pt:$\bullet$:
$K↓2←K↓2+1$, go to $A$.

\disleft 20pt:$\bullet$:
If $K↓1=0$, go to $A$. Otherwise, $K↓1←K↓1-1$, go to $B$.

\disleft 20pt:$\bullet$:
If $K↓2=0$, go to $A$. Otherwise, $K↓2←K↓2-1$, go to $B$.

\disleft 20pt:$\bullet$:
{\tt HALT}.

\smallskip
\noindent
Such a program can be executed in only one way, there being no input mechanism.
It may eventually halt, or it may run forever. It is simple to modify any
program slightly, to clear both counters to zero before halting, and to have
only a single halt state,~$H$.

It is an established result of computability theory that there is no algorithm
that can determine for any OTCM whether it halts or not.

From a given OTCM, one can construct a first order axiom system.

If state $A$ contains the instruction

\halign{\qquad\qquad #\hfil\cr
$K↓1←K↓1+1$, go to $B$\cr}

put in the axiom

\halign{\qquad\qquad #\hfil\cr
$P↓A(x↓1,x↓2)⊃P↓A\bigl(S(x↓1),x↓2\bigr)$.\cr}

The instruction in $A$

\halign{\qquad\qquad #\hfil\cr
If $K↓1=0$, go to $B$; otherwise $K↓1←K↓1-1$, go to $C$\cr}

determines the axiom

\halign{\qquad\qquad #\hfil\cr
$P↓A(\hbox{\bf Z},x↓2)⊃P↓B(\hbox{\bf Z},x↓2)$\cr
$P↓A\bigl(S(x↓1),x↓2\bigr)⊃P↓C(x↓1,x↓2)$\cr}

The instruction

\halign{\qquad\qquad #\hfil\cr
Start, with $K↓1=K↓2=0$, go to $B$ determines the axiom\cr
$P↓B(\hbox{\bf Z},\hbox{\bf Z})$.\cr}

etc.

\medskip
Now we ask whether $P↓H(\hbox{\bf Z},\hbox{\bf Z})$ is 
deducible from this axiom system.

One can interpret the symbols of the axiom system in this way:

\smallskip
\disleft 20pt:$\bullet$:
{\bf Z} is the number zero.

\disleft 20pt:$\bullet$:
$S(x)=x+1$, for any natural number $x$.

\disleft 20pt:$\bullet$:
$P↓A(x↓1,x↓2)$ is true for natural numbers $x$ and $y$ only if the OTCM
program eventually reaches state~$A$ with $x↓1$ in~$K↓1$ and $x↓2$ in~$K↓2$.

\smallskip
\noindent
All the axioms are valid for this interpretation. If the $i↑{\rm th}$ step
of the program reaches state~$A$ with $K↓1$ containing $n↓1$ and $K↓2$
containing~$n↓2$, an easy induction on~$i$ shows that
$\vdash P↓A\bigl(S↑{n↓1}(\hbox{\bf Z}),S↑{n↓2}(\hbox{\bf Z})\bigr)$. 
In particular,
if the OTCM eventually halts, $\vdash P↓H(\hbox{\bf Z},\hbox{\bf Z})$.

Because the axioms are valid for the above interpretation, all theorems
are also valid, and $\vdash P↓H(z,z)$ implies that the OTCM eventually
halts. Therefore

\halign{\qquad\qquad #\hfil\cr
$\vdash P↓H(\hbox{\bf Z},\hbox{\bf Z})$ iff the OTCM halts.\cr}

\smallskip
\noindent
Any algorithm that determines whether $\vdash P↓H(\hbox{\bf Z},\hbox{\bf Z})$, 
also determines
whether the OTCM halts. No such algorithm can  exist. Therefore there
can be no algorithm that determines for every first order axiom system,
and desired conclusion, whether the conclusion is deducible from the
axioms. Even if the axioms are limited to two-place predicates, a single
constant symbol, and a single function symbol, no algorithm exists. We
say that the property of being a theorem in the first order calculus
is undecidable, or in shorthand form:

\smallskip
\halign{\qquad\qquad #\hfil\cr
{\it The first order calculus is undecidable.}\cr}


\bigskip
\parindent0pt
\copyright 1987 Robert W. Floyd.
First draft (not published)
January 2, 1987.
%revised date;
%subsequently revised.

\bye